I don't get the failure of the CI (the one with opam). It looks like it is trying to install analysis 0.2.3...
(By the way, this branch compiles on my computer using the latest MathComp 1.11.0 opam packages.)

@affeldt-aist I've just seen your comment; maybe this is due to the fact the line

- docker exec CI /bin/bash --login -c "opam pin add -n -y -k path coq-mathcomp-${CONTRIB}.dev ."

?

or alternatively, add

version: "dev"

in
https://github.com/math-comp/analysis/blob/master/opam

does not mention a version, so opam takes the first version it is aware from coq-released (0.2.3)

I thought opam pin add . took ./ as the source...

yes but if no version is mentioned, the algorithm is a bit non-intuitive (it does not defaults to dev…)

(There had been a related discussion in a coq issue, I'll try to re-find it just FTR)

OK, the discussion I was thinking about is this PR:

rocq-prover/rocq#11038

which quotes the following comment in the ocaml/opam repo:

ocaml/opam#2932 (comment)

AFAIU, currently opam chooses the version for pinned packages as follow:

1. use the version specified on the command line, if any
2. use the version: field in the opam file of the pinned package, if any
3. use the latest version available in the package repository, if a package with the same name already exists
   [which explains the fact it guessed the 0.2.3 version]
4. ~unknown with opam1 and ~dev (+dev?) with opam2

(but I don't know if this is also documented in the OPAM manual)

(I pushed the fix suggested by @erikmd but now the CI does not trigger the check using opam anymore...)

(I pushed the fix suggested by @erikmd but now the CI does not trigger the check using opam anymore...)

Actually according to this page it seems the build was indeed triggered (but the status feedback was lost on github side):

https://travis-ci.org/github/math-comp/analysis/jobs/696872899

and the error is now different:

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-mathcomp-analysis.dev] no changes from file:///home/coq/analysis

The following dependencies couldn't be met:
  - coq-mathcomp-analysis -> coq-mathcomp-finmap >= 1.5.0
      no matching version

No solution found, exiting

I see. Since coq-mathcomp-finmap is in extra-dev, it fails.

I see. Since coq-mathcomp-finmap is in extra-dev, it fails.

Well, we should not start making packages from the leafs of the dependency graph 😆.
Finmap should be ok, I am currently porting multinomials and should release real-closed soonish... etc

The new error is still puzzling:

# File "./theories/normedtype.v", line 1439, characters 6-22:
# Error: The LHS of ltxI
#     (_ < _ `&` _)%O

There is no ltxI in the source code.

The new error is still puzzling:

# File "./theories/normedtype.v", line 1439, characters 6-22:
# Error: The LHS of ltxI
#     (_ < _ `&` _)%O

There is no ltxI in the source code.

Yeah, the general problem seems to be the wrong codebase is pulled.

It looks like it is pulling 4b3281e.